|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Rozšíření frameworku ANaConDA pro podporu kontraktů s parametry a jejich omezeními
Mužikovská, Monika ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá problematikou kontraktů pro paralelismus. Jedná se o protokol umožňující specifikovat požadavky na atomicitu v paralelních programech a následnou tvorbu automatických nástrojů pro detekci porušení atomicity. Součástí prostředí ANaConDA pro dynamickou analýzu programů je nástroj pro detekci tohoto druhu chyb, ale jeho výsledky mohou být příliš obecné. Cílem práce bylo navrhnout a implementovat metodu, která bude podporovat kontrakty rozšířené o parametry a jejich omezení, což povede k přesnějším výsledkům analýzy. Experimenty provedené pomocí nově vzniklého analyzátoru na programech se známými chybami ukázaly, že díky zahrnutí parametrů do analýzy je možné výsledky zredukovat až o desítky hlášení o situacích, které při zohlednění kontextu nejsou chybné a pouze zbytečně zatěžovaly vývojáře a znesnadňovaly odhalení skutečných chyb.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Rozšíření frameworku ANaConDA pro podporu kontraktů s parametry a jejich omezeními
Mužikovská, Monika ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá problematikou kontraktů pro paralelismus. Jedná se o protokol umožňující specifikovat požadavky na atomicitu v paralelních programech a následnou tvorbu automatických nástrojů pro detekci porušení atomicity. Součástí prostředí ANaConDA pro dynamickou analýzu programů je nástroj pro detekci tohoto druhu chyb, ale jeho výsledky mohou být příliš obecné. Cílem práce bylo navrhnout a implementovat metodu, která bude podporovat kontrakty rozšířené o parametry a jejich omezení, což povede k přesnějším výsledkům analýzy. Experimenty provedené pomocí nově vzniklého analyzátoru na programech se známými chybami ukázaly, že díky zahrnutí parametrů do analýzy je možné výsledky zredukovat až o desítky hlášení o situacích, které při zohlednění kontextu nejsou chybné a pouze zbytečně zatěžovaly vývojáře a znesnadňovaly odhalení skutečných chyb.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
host ::
RSS.